es:event_system{i:l}, e1,e2:es-E(es).
(loc(e2) = loc(e1)  Id)  ((null(es-hist{i:l}(es;e1;e2)))  es-locl(es; e2; e1)) 

latex

Definitions	t  T, P  Q, decidable(P), x:A. B(x), event_system{i:l}, es-E(es), loc(e), Id, prop{i:l}, P  Q, es-locl(es; e; e'), True, P  Q, P  Q, P  Q, b, es-hist{i:l}(es;e1;e2), False, A, [e, e'], null(as), top, subtype(S; T)
Lemmas	es-interval-nil, assert of null, null-map, es-interval wf2, top wf, assert wf, null wf, es-interval wf, es-interval-is-nil, true wf, es-locl wf, Id wf, es-loc wf, es-E wf, event system wf, decidable es-locl